Nuprl Definition : fpf
11,40
postcript
pdf
fpf(
A
;
a
.
B
(
a
)) ==
d
:(
A
List)
(
a
:{
a
:
A
| (
a
d
)}
B
(
a
))
latex
clarification:
fpf(
A
;
a
.
B
(
a
)) ==
d
:(
A
List)
(
a
:{
a
:
A
| (
a
d
A
)}
B
(
a
))
latex
Definitions
x
:
A
B
(
x
)
,
type
List
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
(
x
l
)
FDL editor aliases
fpf
origin
(a:{a:A| (a 
d)} 
B(a))
(a:{a:A| (a d A)} B(a)) (a:{a:A| (a d)} B(a))
(a:{a:A| (a d A)} B(a)) B(x)B(x) l)